package prolog.terms
import prolog.fluents.DataBase

class Prog(val db: DataBase) extends Source {
  def this() = this(new DataBase(null))
  def this(fname: String) = this(new DataBase(fname))

  type CLAUSE = List[Term]
  type GOAL = List[Term]

  val trail = new Trail()
  val orStack = new ObjectStack[Unfolder]()

  //val db = new DataBase(fname)

  var topgoal: GOAL = null
  var answer: Term = null
  var query: GOAL = null

  var isStopped = true

  def set_query(answer: Term, query: GOAL) = {
    orStack.clear()
    trail.clear()
    this.answer = answer
    this.query = query
    this.topgoal = reduceBuiltins(query)
    pushUnfolder(topgoal)
    isStopped = topgoal.eq(null)
  }

  def set_query(query: GOAL) {
    set_query(null, query: GOAL)
  }

  def pushUnfolder(g: GOAL) {
    if (!g.eq(null) && !g.isEmpty) {
      val cs = db.matches(g)
      //println("cs=" + cs)
      if (!cs.eq(null)) {
        val u = new Unfolder(this, g, cs.iterator)
        orStack.push(u)
      }
    }
  }

  def reduceBuiltins(goal: GOAL): GOAL = {
    var newgoal = goal
    if (!newgoal.isEmpty) {
      var ret = 1
      while (ret > 0 && !newgoal.isEmpty) {
        ret = newgoal.head.ref.exec(this)
        if (ret >= 0) newgoal = newgoal.tail
      }
      if (0 == ret) newgoal = null
    }
    newgoal
  }

  def getTrail: Trail = trail

  override def getElement(): Term = {
    if (isStopped) return null

    var newgoal: GOAL = null
    var more = true
    while (more && !orStack.isEmpty) {
      val step: Unfolder = orStack.pop()

      newgoal = step.nextGoal()
      if (step.notLastClause) orStack.push(step)

      newgoal =
        if (newgoal.eq(null)) null
        else reduceBuiltins(newgoal)

      if (Nil == newgoal) more = false
      else pushUnfolder(newgoal)

      // "no push when null" eventually stops it but only when orStack.isEmpty
    }

    if (newgoal.eq(null)) {
      stop()
      if (!topgoal.isEmpty) return null
    }

    if (null == answer) {
      val conj: Term = query match {
        case Nil => stop()
        case head :: Nil => head
        case xs => {
          Conj.fromList(xs)
        }
      }
      conj
    } else {
      if (query.isEmpty) stop()
      answer
    }
  }

  override def stop(): Term = {
    if (!isStopped) {
      //if (null != trail) trail.unwind(0)
      orStack.clear()
      isStopped = true
    } else
      trail.unwind(0)
    null
  }
}